fpf-sub(A; a.B(a); eq; f; g)
== x:A. 
== (fpf-dom(eq; x; f))  ((fpf-dom(eq; x; g)) c (fpf-ap(f; eq; x) = fpf-ap(g; eq; x))) 

latex

---

clarification:

fpf-sub(A; a.B(a); eq; f; g)
== x:A. 
== (fpf-dom(eq; x; f))
==  ((fpf-dom(eq; x; g)) c (fpf-ap(f; eq; x) = fpf-ap(g; eq; x)  B(x))) 

latex

Definitions	x:A. B(x), P  Q, A c B, b, fpf-dom(eq; x; f), fpf-ap(f; eq; x)
FDL editor aliases	fpf-sub